Normal(da) == k:Knd. (k  dom(da))  Normal(da(k).1) 

latex

---

clarification:

normal-ma-da{i:l}
normal-ma-da(da)
== k:Knd. (fpf-dom(KindDeq; k; da))  normal-type{i:l}((daKindDeq(k).1)) 

latex

Definitions	KindDeq, f(x), t.1, Normal(T), x  dom(f), b, P  Q, Knd, x:A. B(x)
FDL editor aliases	normal-ma-da